{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, EmptyDataDecls #-}

{-# LANGUAGE TemplateHaskell #-}

{- |

Module      :  Data.Yoko.Core
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

The core structural types; \"sum of products\" and such.

-}

module Data.Yoko.Core where

import Type.Yoko.Type (derive)
import Type.Yoko.TSTSS

--import Polarity



-- | Structural representations (e.g. "Data.Yoko.Generic"'s 'RM') of a @*@ type
-- can be derived as a data family indexed by the core representation (@Rep@)
-- of that type.
type family Rep a



-- | void
data V
-- | unit
data U = U
-- | a dependency
newtype D a = D a
-- | a recursive occurrence
newtype R t = R t
-- | argument to a @* -> *@
newtype F f c = F (f c)
-- | arguments to a @* -> * -> *@
newtype FF ff c d = FF (ff c d)
-- | meta information
newtype M i c = M c

-- | adjacent fields, isomorhpic to FF (,)
infixr 6 :*
data c :* d = c :* d
type AF = (:*)

-- | a named intermediate (user hook); crucially: @type instance Rep (N t) =
-- Rep t@.
newtype N t = N t

type instance Rep (N t) = Rep t   -- this is the crucial meaning of N



concat `fmap` mapM derive [''V, ''U, ''D, ''R, ''F, ''FF, ''M, ''(:*), ''N]





{-
type instance Polarity ([qK|*->*->*|] M) (ki :* kt :* U) = Neutral
type instance Polarity ([qK|*->*|] (M i)) (kt :* U) = Pos

type instance Polarity ([qK|*->*|] R) (ka :* U) = Pos

type instance Polarity ([qK|(*->*)->*->*|] F) (kf :* kt :* U) = Pos
type instance Polarity ([qK|*->*|] (F f)) (kt :* U) =
  Polarity ([qK|*->*|] f) (kt :* U)

type instance Polarity ([qK|(*->*->*)->*->*->*|] FF) (kff :* kt :* ks :* U) = Pos
type instance Polarity ([qK|*->*->*|] (FF ff)) (kt :* ks :* U) =
  Polarity ([qK|*->*->*|] ff) (kt :* ks :* U)
type instance Polarity ([qK|*->*|] (FF ff t)) (ks :* U) =
  Polarity ([qK|*->*|] (ff t)) (ks :* U)
-}




type family Gst c
type instance Gst (F f c) = f (Gst c)
type instance Gst (FF ff c d) = ff (Gst c) (Gst d)
type instance Gst (D a) = a
type instance Gst (M i c) = Gst c
type instance Gst (R t) = t
type instance Gst U = ()
type instance Gst V = V
type instance Gst (N n) = Gst (Rep n)

-- @gist@ folds the mediator @m@ into the type and forgets all the frippery of
-- the core representation. (The opposite of \"gist\" is \"frippery\".)
class Gist c where gist :: c -> Gst c; frip :: Gst c -> c

instance (Functor f, Gist c) => Gist (F f c) where
  gist (F x) = fmap gist x; frip = F . fmap frip
instance (FunctorTSTSS ff, Gist c, Gist d) => Gist (FF ff c d) where
  gist ~(FF x) = fmapTSTSS gist gist $ x
  frip = FF . fmapTSTSS frip frip
instance Gist (D a) where gist (D x) = x; frip = D
instance Gist c => Gist (M i c) where
  gist ~(M x) = gist x; frip = M . frip
instance Gist (R t) where gist (R x) = x; frip = R
instance Gist U where gist _ = (); frip _ = U

instance (Generic t, Gist (Rep t)) => Gist (N t) where
  gist = gist . rep; frip = obj . frip
class Generic a where rep :: N a -> Rep a; obj :: Rep a -> N a
